m, m', a, a', b, b':.
m = m'  (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m')) 

latex

Definitions	P  Q, P & Q, P  Q, P  Q, a = b mod m, x:A. B(x), Prop, t  T
Lemmas	eqmod transitivity, eqmod inversion, eqmod wf